Vers une approche formelle pour la validation des protocoles d’interaction en systèmes multi-agents
Identifieur interne : 004237 ( Main/Exploration ); précédent : 004236; suivant : 004238Vers une approche formelle pour la validation des protocoles d’interaction en systèmes multi-agents
Auteurs : Hind Fadil [France] ; Jean-Luc Koning [France]Source :
- Ingénierie des systèmes d'information [ 1633-1311 ] ; 2008.
Abstract
Les travaux de recherche relevant du domaine des systèmes multi-agents se sont largement intéressés à la définition de protocoles d’interaction en vue de régir les communications entre agents. Néanmoins, ces protocoles sont souvent informels (décrits par des textes) ou semi-formels (décrits par des diagrammes), et manquent, par conséquent, de bases théoriques solides permettant de prouver leur correction. Il est donc important de mettre en œuvre une méthodologie stricte et abordable pour spécifier, concevoir et vérifier les protocoles d’interaction de ces systèmes. Pour cela, l’usage d’une méthode formelle, telle que B, présente des avantages indéniables. Dans le cadre de notre investigation, nous proposons, dans un premier temps, une passerelle entre une modélisation semi-formelle en AUML et sa contre-partie formelle en B. Ensuite, nous montrons l’apport de notre démarche en injectant dans la spécification formelle une formalisation d’un ensemble de propriétés élémentaires telles que la cohérence des messages, la pertinence des protocoles et des rôles, etc.
Research works interested by multi-agent systems have been essentially focused on how to define interaction protocoles in order to manage inter-agent communication. However these agent interaction protocols have often been described in informal ways (using natural language) or in semi-formal ways (by diagrams). Hence, they lack sound theoretical bases that would prove they are correct. Thus, it seems important to clearly define a design methodology which allows to specify and check these system’s interaction protocols. In this context, formal methods, such as B, provide a useful contribution. In our investigation, we propose to bridge the gap between a semi-formal modeling in AUML and its formal counterpart in B. Then, we prove how well our approach performs by inserting into the resulting formal specification a number of formal elementary properties such as message coherence, protocols and roles relevance, etc.
Url:
DOI: 10.3166/isi.13.2.33-52
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000387
- to stream Istex, to step Curation: 000385
- to stream Istex, to step Checkpoint: 000C64
- to stream Main, to step Merge: 004348
- to stream Main, to step Curation: 004237
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="fr">Vers une approche formelle pour la validation des protocoles d’interaction en systèmes multi-agents</title><author><name sortKey="Fadil, Hind" sort="Fadil, Hind" uniqKey="Fadil H" first="Hind" last="Fadil">Hind Fadil</name></author><author><name sortKey="Koning, Jean Luc" sort="Koning, Jean Luc" uniqKey="Koning J" first="Jean-Luc" last="Koning">Jean-Luc Koning</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:11091AD313D4B6A6B5CE908C04211005FFFC893F</idno><date when="2008" year="2008">2008</date><idno type="doi">10.3166/isi.13.2.33-52</idno><idno type="url">https://api.istex.fr/ark:/67375/HT0-1D3BJR2Z-3/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000387</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000387</idno><idno type="wicri:Area/Istex/Curation">000385</idno><idno type="wicri:Area/Istex/Checkpoint">000C64</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000C64</idno><idno type="wicri:doubleKey">1633-1311:2008:Fadil H:vers:une:approche</idno><idno type="wicri:Area/Main/Merge">004348</idno><idno type="wicri:Area/Main/Curation">004237</idno><idno type="wicri:Area/Main/Exploration">004237</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="fr">Vers une approche formelle pour la validation des protocoles d’interaction en systèmes multi-agents</title><author><name sortKey="Fadil, Hind" sort="Fadil, Hind" uniqKey="Fadil H" first="Hind" last="Fadil">Hind Fadil</name><affiliation wicri:level="0"><country wicri:rule="zip">France</country></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Koning, Jean Luc" sort="Koning, Jean Luc" uniqKey="Koning J" first="Jean-Luc" last="Koning">Jean-Luc Koning</name><affiliation wicri:level="0"><country wicri:rule="zip">France</country></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="j" type="main">Ingénierie des systèmes d'information</title><title level="j" type="abbrev">Ing. Sys. Info.</title><idno type="ISSN">1633-1311</idno><idno type="eISSN">2116-7125</idno><imprint><publisher>Lavoisier</publisher><date type="published" when="2008-03">2008</date><biblScope unit="vol">13</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="33">33</biblScope><biblScope unit="page" to="52">52</biblScope><biblScope unit="page-count">20</biblScope><biblScope unit="ref-count">0</biblScope><biblScope unit="fig-count">0</biblScope><biblScope unit="table-count">0</biblScope></imprint><idno type="ISSN">1633-1311</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">1633-1311</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr">Les travaux de recherche relevant du domaine des systèmes multi-agents se sont largement intéressés à la définition de protocoles d’interaction en vue de régir les communications entre agents. Néanmoins, ces protocoles sont souvent informels (décrits par des textes) ou semi-formels (décrits par des diagrammes), et manquent, par conséquent, de bases théoriques solides permettant de prouver leur correction. Il est donc important de mettre en œuvre une méthodologie stricte et abordable pour spécifier, concevoir et vérifier les protocoles d’interaction de ces systèmes. Pour cela, l’usage d’une méthode formelle, telle que B, présente des avantages indéniables. Dans le cadre de notre investigation, nous proposons, dans un premier temps, une passerelle entre une modélisation semi-formelle en AUML et sa contre-partie formelle en B. Ensuite, nous montrons l’apport de notre démarche en injectant dans la spécification formelle une formalisation d’un ensemble de propriétés élémentaires telles que la cohérence des messages, la pertinence des protocoles et des rôles, etc.</div><div type="abstract" xml:lang="en">Research works interested by multi-agent systems have been essentially focused on how to define interaction protocoles in order to manage inter-agent communication. However these agent interaction protocols have often been described in informal ways (using natural language) or in semi-formal ways (by diagrams). Hence, they lack sound theoretical bases that would prove they are correct. Thus, it seems important to clearly define a design methodology which allows to specify and check these system’s interaction protocols. In this context, formal methods, such as B, provide a useful contribution. In our investigation, we propose to bridge the gap between a semi-formal modeling in AUML and its formal counterpart in B. Then, we prove how well our approach performs by inserting into the resulting formal specification a number of formal elementary properties such as message coherence, protocols and roles relevance, etc.</div></front></TEI><affiliations><list><country><li>France</li></country></list><tree><country name="France"><noRegion><name sortKey="Fadil, Hind" sort="Fadil, Hind" uniqKey="Fadil H" first="Hind" last="Fadil">Hind Fadil</name></noRegion><name sortKey="Fadil, Hind" sort="Fadil, Hind" uniqKey="Fadil H" first="Hind" last="Fadil">Hind Fadil</name><name sortKey="Koning, Jean Luc" sort="Koning, Jean Luc" uniqKey="Koning J" first="Jean-Luc" last="Koning">Jean-Luc Koning</name><name sortKey="Koning, Jean Luc" sort="Koning, Jean Luc" uniqKey="Koning J" first="Jean-Luc" last="Koning">Jean-Luc Koning</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004237 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004237 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:11091AD313D4B6A6B5CE908C04211005FFFC893F
|texte= Vers une approche formelle pour la validation des protocoles d’interaction en systèmes multi-agents
}}
| This area was generated with Dilib version V0.6.33. |  |